(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 3))
(declare-fun v1 () (_ BitVec 7))
(declare-fun v2 () (_ BitVec 4))
(assert (let ((e3(_ bv3 5)))
(let ((e4 ((_ extract 2 1) v2)))
(let ((e5 (ite (= ((_ sign_extend 2) e3) v1) (_ bv1 1) (_ bv0 1))))
(let ((e6 ((_ sign_extend 3) e5)))
(let ((e7 (ite (= (_ bv1 1) ((_ extract 0 0) e5)) ((_ sign_extend 1) v2) e3)))
(let ((e8 (ite (= (_ bv1 1) ((_ extract 1 1) e4)) v1 v1)))
(let ((e9 ((_ extract 0 0) e4)))
(let ((e10 ((_ extract 2 0) v2)))
(let ((e11 (ite (= e3 ((_ zero_extend 1) v2)) (_ bv1 1) (_ bv0 1))))
(let ((e12 ((_ sign_extend 3) e4)))
(let ((e13 ((_ sign_extend 2) e12)))
(let ((e14 (ite (distinct e13 ((_ zero_extend 4) e10)) (_ bv1 1) (_ bv0 1))))
(let ((e15 ((_ sign_extend 0) e10)))
(let ((e16 ((_ extract 2 1) e10)))
(let ((e17 ((_ zero_extend 0) e5)))
(let ((e18 ((_ sign_extend 3) e15)))
(let ((e19 ((_ zero_extend 0) e15)))
(let ((e20 ((_ extract 0 0) e16)))
(let ((e21 ((_ extract 1 1) e8)))
(let ((e22 (ite (distinct ((_ zero_extend 3) v2) v1) (_ bv1 1) (_ bv0 1))))
(let ((e23 ((_ extract 6 3) e8)))
(let ((e24 ((_ zero_extend 0) e20)))
(let ((e25 (ite (= e23 ((_ sign_extend 3) e24)) (_ bv1 1) (_ bv0 1))))
(let ((e26 ((_ sign_extend 0) e13)))
(let ((e27 ((_ sign_extend 0) v1)))
(let ((e28 ((_ extract 0 0) e22)))
(let ((e29 ((_ extract 0 0) e9)))
(let ((e30 ((_ sign_extend 1) e3)))
(let ((e31 ((_ sign_extend 2) e20)))
(let ((e32 (concat e4 e7)))
(let ((e33 (ite (= e27 ((_ sign_extend 2) e7)) (_ bv1 1) (_ bv0 1))))
(let ((e34 (ite (= e13 ((_ sign_extend 6) e5)) (_ bv1 1) (_ bv0 1))))
(let ((e35 (ite (= (_ bv1 1) ((_ extract 0 0) v1)) e26 ((_ zero_extend 1) e30))))
(let ((e36 ((_ sign_extend 0) e30)))
(let ((e37 ((_ sign_extend 0) e13)))
(let ((e38 ((_ sign_extend 1) e33)))
(let ((e39 ((_ extract 3 3) e36)))
(let ((e40 ((_ extract 0 0) e39)))
(let ((e41 ((_ extract 0 0) e9)))
(let ((e42 ((_ sign_extend 0) e33)))
(let ((e43 (ite (= e8 e26) (_ bv1 1) (_ bv0 1))))
(let ((e44 (ite (distinct e20 e14) (_ bv1 1) (_ bv0 1))))
(let ((e45 ((_ zero_extend 5) e42)))
(let ((e46 ((_ zero_extend 2) e24)))
(let ((e47 ((_ extract 0 0) e14)))
(let ((e48 ((_ extract 0 0) e9)))
(let ((e49 ((_ sign_extend 1) e10)))
(let ((e50 (ite (= (_ bv1 1) ((_ extract 0 0) e42)) v0 ((_ zero_extend 2) e11))))
(let ((e51 (= e32 ((_ zero_extend 4) v0))))
(let ((e52 (distinct e16 ((_ sign_extend 1) e20))))
(let ((e53 (distinct e23 ((_ zero_extend 3) e22))))
(let ((e54 (= e50 e31)))
(let ((e55 (distinct e10 ((_ zero_extend 2) e20))))
(let ((e56 (distinct v2 ((_ sign_extend 3) e20))))
(let ((e57 (= e37 ((_ zero_extend 3) e6))))
(let ((e58 (= e6 ((_ sign_extend 3) e39))))
(let ((e59 (distinct ((_ sign_extend 3) e31) e18)))
(let ((e60 (= e5 e29)))
(let ((e61 (= e23 ((_ zero_extend 3) e20))))
(let ((e62 (distinct ((_ zero_extend 4) e19) e35)))
(let ((e63 (= ((_ sign_extend 5) e47) e18)))
(let ((e64 (distinct ((_ zero_extend 4) e10) e32)))
(let ((e65 (= ((_ zero_extend 1) e20) e4)))
(let ((e66 (distinct v0 ((_ zero_extend 2) e29))))
(let ((e67 (= ((_ zero_extend 3) e23) e26)))
(let ((e68 (= v1 ((_ zero_extend 4) e46))))
(let ((e69 (= ((_ zero_extend 1) e44) e4)))
(let ((e70 (= e35 ((_ zero_extend 4) e15))))
(let ((e71 (= e37 ((_ sign_extend 4) e10))))
(let ((e72 (= e27 ((_ zero_extend 6) e17))))
(let ((e73 (= e11 e17)))
(let ((e74 (= ((_ sign_extend 3) e29) e49)))
(let ((e75 (= e49 ((_ zero_extend 1) e50))))
(let ((e76 (distinct ((_ zero_extend 3) e24) e23)))
(let ((e77 (distinct e8 ((_ sign_extend 6) e47))))
(let ((e78 (= e18 ((_ zero_extend 4) e38))))
(let ((e79 (distinct ((_ sign_extend 6) e9) e26)))
(let ((e80 (distinct e10 e10)))
(let ((e81 (distinct e38 ((_ sign_extend 1) e29))))
(let ((e82 (= e20 e48)))
(let ((e83 (= ((_ zero_extend 2) e21) e46)))
(let ((e84 (distinct e49 ((_ sign_extend 3) e42))))
(let ((e85 (distinct e46 e50)))
(let ((e86 (distinct e47 e11)))
(let ((e87 (distinct e37 ((_ zero_extend 2) e7))))
(let ((e88 (distinct ((_ zero_extend 6) e33) e32)))
(let ((e89 (= ((_ zero_extend 4) e16) e36)))
(let ((e90 (= e32 ((_ zero_extend 4) e10))))
(let ((e91 (distinct e31 ((_ sign_extend 2) e11))))
(let ((e92 (distinct e26 ((_ sign_extend 6) e40))))
(let ((e93 (= e28 e11)))
(let ((e94 (distinct e36 ((_ sign_extend 5) e42))))
(let ((e95 (distinct e11 e33)))
(let ((e96 (= e37 e35)))
(let ((e97 (distinct e10 ((_ zero_extend 2) e39))))
(let ((e98 (= e37 ((_ sign_extend 6) e33))))
(let ((e99 (= ((_ zero_extend 3) e4) e7)))
(let ((e100 (distinct ((_ zero_extend 1) e4) e19)))
(let ((e101 (= e28 e43)))
(let ((e102 (distinct e49 ((_ zero_extend 1) e50))))
(let ((e103 (= ((_ zero_extend 6) e47) e32)))
(let ((e104 (= e31 ((_ sign_extend 2) e17))))
(let ((e105 (= e50 ((_ zero_extend 2) e34))))
(let ((e106 (distinct e42 e34)))
(let ((e107 (= ((_ sign_extend 2) e40) v0)))
(let ((e108 (distinct ((_ zero_extend 1) e41) e16)))
(let ((e109 (distinct ((_ zero_extend 2) e10) e3)))
(let ((e110 (distinct ((_ zero_extend 6) e9) v1)))
(let ((e111 (= e35 ((_ sign_extend 6) e22))))
(let ((e112 (distinct e36 ((_ sign_extend 5) e42))))
(let ((e113 (distinct ((_ sign_extend 2) e25) e19)))
(let ((e114 (= ((_ sign_extend 5) e20) e30)))
(let ((e115 (= e15 ((_ zero_extend 2) e5))))
(let ((e116 (= ((_ sign_extend 3) e39) e6)))
(let ((e117 (= e35 ((_ sign_extend 6) e39))))
(let ((e118 (distinct ((_ sign_extend 5) e11) e36)))
(let ((e119 (= e46 ((_ zero_extend 2) e33))))
(let ((e120 (= ((_ zero_extend 1) e12) e45)))
(let ((e121 (distinct ((_ zero_extend 5) e21) e36)))
(let ((e122 (distinct e9 e42)))
(let ((e123 (= ((_ zero_extend 2) e39) e10)))
(let ((e124 (distinct e7 ((_ zero_extend 4) e41))))
(let ((e125 (distinct ((_ zero_extend 2) e19) e12)))
(let ((e126 (= e26 e26)))
(let ((e127 (= ((_ sign_extend 1) e5) e16)))
(let ((e128 (distinct ((_ sign_extend 5) e39) e30)))
(let ((e129 (= e20 e22)))
(let ((e130 (distinct e21 e17)))
(let ((e131 (distinct ((_ sign_extend 4) e15) e13)))
(let ((e132 (distinct e33 e22)))
(let ((e133 (= e50 ((_ zero_extend 1) e38))))
(let ((e134 (= e6 ((_ sign_extend 3) e20))))
(let ((e135 (distinct ((_ zero_extend 1) e12) e45)))
(let ((e136 (distinct ((_ sign_extend 3) e33) e6)))
(let ((e137 (= e17 e17)))
(let ((e138 (= ((_ sign_extend 5) e22) e30)))
(let ((e139 (= ((_ zero_extend 2) e28) e15)))
(let ((e140 (= e34 e28)))
(let ((e141 (= e35 ((_ sign_extend 1) e30))))
(let ((e142 (distinct e37 e8)))
(let ((e143 (distinct e20 e39)))
(let ((e144 (distinct e34 e40)))
(let ((e145 (= ((_ zero_extend 6) e39) e27)))
(let ((e146 (= e26 ((_ zero_extend 6) e44))))
(let ((e147 (distinct ((_ zero_extend 4) e28) e12)))
(let ((e148 (distinct e29 e41)))
(let ((e149 (= ((_ zero_extend 5) e20) e30)))
(let ((e150 (distinct ((_ sign_extend 4) e9) e12)))
(let ((e151 (distinct ((_ zero_extend 3) e40) e23)))
(let ((e152 (distinct e17 e41)))
(let ((e153 (= e29 e14)))
(let ((e154 (xor e108 e60)))
(let ((e155 (ite e113 e71 e125)))
(let ((e156 (ite e123 e81 e86)))
(let ((e157 (=> e124 e107)))
(let ((e158 (or e105 e78)))
(let ((e159 (= e140 e136)))
(let ((e160 (or e68 e77)))
(let ((e161 (not e142)))
(let ((e162 (not e79)))
(let ((e163 (xor e96 e83)))
(let ((e164 (= e98 e91)))
(let ((e165 (= e116 e129)))
(let ((e166 (xor e106 e73)))
(let ((e167 (= e143 e74)))
(let ((e168 (not e152)))
(let ((e169 (ite e70 e150 e138)))
(let ((e170 (not e145)))
(let ((e171 (or e52 e88)))
(let ((e172 (not e160)))
(let ((e173 (and e146 e166)))
(let ((e174 (not e147)))
(let ((e175 (and e131 e120)))
(let ((e176 (not e165)))
(let ((e177 (and e115 e64)))
(let ((e178 (or e171 e139)))
(let ((e179 (= e159 e162)))
(let ((e180 (=> e59 e133)))
(let ((e181 (and e118 e132)))
(let ((e182 (xor e54 e148)))
(let ((e183 (and e65 e157)))
(let ((e184 (and e58 e90)))
(let ((e185 (xor e170 e55)))
(let ((e186 (xor e169 e144)))
(let ((e187 (xor e104 e128)))
(let ((e188 (= e154 e117)))
(let ((e189 (xor e187 e168)))
(let ((e190 (or e119 e57)))
(let ((e191 (and e109 e94)))
(let ((e192 (and e72 e190)))
(let ((e193 (ite e62 e80 e69)))
(let ((e194 (xor e76 e156)))
(let ((e195 (=> e130 e66)))
(let ((e196 (ite e51 e161 e183)))
(let ((e197 (not e149)))
(let ((e198 (ite e189 e184 e151)))
(let ((e199 (not e121)))
(let ((e200 (ite e197 e188 e85)))
(let ((e201 (= e164 e158)))
(let ((e202 (=> e176 e92)))
(let ((e203 (=> e122 e185)))
(let ((e204 (and e173 e137)))
(let ((e205 (not e134)))
(let ((e206 (= e178 e199)))
(let ((e207 (xor e206 e201)))
(let ((e208 (= e63 e174)))
(let ((e209 (= e192 e191)))
(let ((e210 (or e56 e172)))
(let ((e211 (xor e208 e177)))
(let ((e212 (= e84 e84)))
(let ((e213 (=> e100 e179)))
(let ((e214 (= e207 e102)))
(let ((e215 (or e214 e211)))
(let ((e216 (and e155 e95)))
(let ((e217 (= e194 e93)))
(let ((e218 (not e181)))
(let ((e219 (or e82 e212)))
(let ((e220 (and e203 e198)))
(let ((e221 (ite e219 e186 e67)))
(let ((e222 (ite e175 e182 e218)))
(let ((e223 (ite e114 e200 e153)))
(let ((e224 (=> e205 e204)))
(let ((e225 (not e223)))
(let ((e226 (not e126)))
(let ((e227 (or e213 e167)))
(let ((e228 (=> e75 e141)))
(let ((e229 (or e112 e97)))
(let ((e230 (not e110)))
(let ((e231 (=> e221 e87)))
(let ((e232 (xor e224 e228)))
(let ((e233 (=> e193 e230)))
(let ((e234 (and e217 e222)))
(let ((e235 (xor e227 e135)))
(let ((e236 (= e234 e235)))
(let ((e237 (=> e215 e196)))
(let ((e238 (or e233 e216)))
(let ((e239 (xor e238 e163)))
(let ((e240 (and e89 e53)))
(let ((e241 (= e180 e99)))
(let ((e242 (or e103 e202)))
(let ((e243 (= e242 e127)))
(let ((e244 (and e237 e236)))
(let ((e245 (and e240 e243)))
(let ((e246 (or e226 e220)))
(let ((e247 (xor e244 e239)))
(let ((e248 (ite e61 e209 e101)))
(let ((e249 (or e245 e245)))
(let ((e250 (=> e225 e231)))
(let ((e251 (and e232 e195)))
(let ((e252 (or e229 e248)))
(let ((e253 (= e252 e252)))
(let ((e254 (xor e246 e250)))
(let ((e255 (= e254 e254)))
(let ((e256 (or e249 e210)))
(let ((e257 (and e251 e111)))
(let ((e258 (ite e256 e256 e247)))
(let ((e259 (xor e241 e257)))
(let ((e260 (=> e253 e259)))
(let ((e261 (not e255)))
(let ((e262 (and e261 e260)))
(let ((e263 (=> e262 e262)))
(let ((e264 (xor e263 e263)))
(let ((e265 (or e264 e258)))
e265
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
